 \documentclass[12pt,compress]{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{myproof}


%\usepackage{japerez}
% Davides's macro
\usepackage{davidemacro}
\usepackage{evolvablemacro}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

%\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}

\hypersetup{%
	pdftitle={Adaptable Processes},%
	pdfauthor={Jorge A. Perez},%
	pdfsubject={},%
	pdfkeywords={process calculi, concurrency}%
}

\usepackage{color}
%\newcommand{\emphcolor}[1]{\textcolor{orange}{#1}\xspace}
\newcommand{\emphcolor}[1]{\textcolor{purple}{#1}\xspace}
\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}
\newcommand{\emphcolorm}[1]{\textcolor{magenta}{#1}\xspace}

\newcommand{\whitecolor}[1]{\textcolor{white}{#1}\xspace}
\newcommand{\hidecolor}[1]{\textcolor{darkgray}{#1}\xspace}
\newcommand{\olivecolor}[1]{\textcolor{olive}{#1}\xspace}

%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,

\newcommand{\tealtext}[1]{\textcolor{teal}{#1}\xspace}

\newcommand{\str}[1]{\structure{#1}}


%\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}
%\newcommand{\til}[1]{\widetilde{#1}}
%\newcommand{\update}[2]{\til{#1}\{#2\} } 
%\newcommand{\component}[2]{#1 [#2]   }  %a[P]
%\newcommand{\outC}[1]{\overline{#1}}      % CCS  output

\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\bbl}[1]{\begin{block}{#1}}
\newcommand{\ebl}{\end{block}}

% Context
\newcommand{\ol}{\langle\!\langle}
\newcommand{\cl}{\rangle\!\rangle}
\newcommand{\hl}[1]{\ol #1 \cl}
\newcommand{\fillcon}[2]{\ensuremath{#1\hl{#2}}}

\newcommand{\pired}{\longrightarrow}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\rulename}[1]{\textsc{(#1)}}

\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\midef}{\ensuremath{\stackrel{\mathsf{def}}{=}}}



%\newcommand{\str}[1]{\structure{#1}}
\newcommand{\fkspc}{{\tiny \ }\\}


\title[Adaptable Processes]{Adaptable Processes}
\author[Cinzia Di Giusto]{ Mario Bravetti ~~Cinzia Di Giusto  ~~ \emphcolor{Jorge A. P\'erez} ~~ Gianluigi Zavattaro}
%\date[June 8, 2011]{GLOSS Seminar, FCUL - September 15, 2011}
\date{CITI Seminar, DI - FCTUNL - October 26, 2011}
  
\institute[INRIA Rh\^onealpes]{Universit\`a di Bologna ~
INRIA Rh\^{o}ne-Alpes ~
\emphcolor{CITI-DI - FCT UNL}}

\setbeamertemplate{navigation symbols}{} 

\usecolortheme{default}
%\useoutertheme{progressbar}
%\useinnertheme{progressbar}
%\usefonttheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}

\begin{document}



\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}


\frame{
\frametitle{This talk in one slide}
\str{Adaptable processes}
\be
\item A \str{formal} model of  \emphcolor{evolvable} communicating processes \\
Processes can be discarded, stopped, relocated at runtime \pause 
\item Two \emphcolor{verification problems} for adaptable processes: \\
They describe bounded and unbounded \emphcolor{error repetition}   \pause 
\item Unfortunately, both problems are \emphcolor{undecidable}, so decision procedures for verification \emphcolor{do not exist} \pause
\item We investigate  \emphcolor{fragments} of adaptable processes where the problems 
are \emphcolor{decidable}
\ee
}

\begin{frame}
\frametitle{Roadmap}

\tableofcontents

\end{frame}

\AtBeginSection[]
{
  \begin{frame}
\setcounter{tocdepth}{3}
%\tableofcontents

      \frametitle{Roadmap}
      \tableofcontents[currentsection] 
  \end{frame}
}

\section{Motivation}

\begin{frame}
\frametitle{Context (very broad)}

Modern computing systems are increasingly
\begin{itemize}
\item \str{concurrent}
\begin{itemize}
\item multiple interacting entities, usually distributed \pause
\end{itemize}
\item \str{infinite} \pause
\begin{itemize}
\item termination is a \emphcolor{local} property
\item tolerant to \emphcolor{unexpected conditions} (e.g. failures) \pause 
\item but also able to \emphcolor{dynamically reconfigure} themselves \\ (e.g. performance and maintenance reasons)
\end{itemize}
\end{itemize}
\end{frame}


\frame{
\frametitle{The process calculi approach}
\begin{center}
%A \str{} to the analysis of \str{evolvable systems} 

%\pause

\bi
\item Identify some \str{phenomenon of interest} 
\item Isolate \str{basic construct(s)} for it, and define a \str{calculus}
\item Study the \str{properties} of the calculus (and systems modeled in it) and define \str{reasoning techniques} for it
\ei
\end{center}

%\pause

%We are mainly concerned with \emphcolor{dynamic reconfiguration} issues:\\
%\begin{itemize}
%\item finding proper \emphcolor{constructs} for representing evolution 
%\item defining \emphcolor{correctness properties} for evolvable systems
%\end{itemize}


%\pause
%
%\begin{block}{Our choices}
%\bi
%\item The phenomena: \str{components} and their \str{evolution}
%\item The calculus: $\mathcal{E}$, a core language with \str{updatable} components
%\item The properties: \str{(un)decidability} of component  \str{adaptation}
%\ei
%\end{block}

}

\frame{
\frametitle{Our base language: Milner's CCS}
\bi
\item CCS abstracts \str{concurrent  systems} into \\ \str{communicating processes} which interact via handshake 
\item It has been intensively studied in the last 10-20 years. \\ Many theoretical results
\bi 
\item behavioral equivalences 
\item logics 
\item \emphcolor{expressiveness and decidability}
\ei
 as well as software tools.
\item Together with the \str{$\pi$-calculus} (CCS's name-passing extension) are the most representative process calculi
\ei
}

\frame{
\frametitle{Our base language: Milner's CCS}

\str{Syntax.~} Assume an countable infinite collection of \str{names} $\mathcal{N}$, \\ and a complementary set of
\str{co-names} $\overline{\mathcal{N}} = \{\overline{a} \mid a \in \mathcal{N}\}$. \\
Let $\mathcal{L} = \mathcal{N} \cup \overline{\mathcal{N}}$ be a set of \str{prefixes}. %, and let $\mathcal{L} \cup \tau$ be the \str{actions}.
\pause
\vspace{0.2cm}
\[
\hspace{-6mm}
\begin{array}{rcll}
P,Q & :: = &  \sum_{i \in I} \pi_{i}.P_{i}    ~& \mbox{choice among all $\pi_{i}.P_{i}$ with $\pi_{i} \in \mathcal{L}$}\\[\mypt]
 & \midd &  P \parallel Q & \mbox{parallel composition (concurrency)} \\[\mypt]
 & \midd &  !\pi.P & \mbox{infinitely many copies of $P$ with trigger $\pi$} \\[\mypt]
 & \midd &  (\nu \til{n})P & \mbox{name restriction: $\til{n}$ are bound in $P$} 
\end{array} 
 \]
\pause
\vspace{0.4cm}

Two special cases of the choice operator: \\
~~~The \str{inactive} process  $\nil$ (when the sum is empty)\\
~~~The \str{binary choice} $\pi_{1}.P_{1} + \pi_{2}.P_{2}$ (when ${|}I{|}=2$).

Also, we write $\prod_{i \in I} P_{i}$ to abbreviate $P_{1} \parallel P_{2} \parallel \cdots \parallel P_{n}$
}

\frame{
\frametitle{Our base language: Milner's CCS}

\str{Operational Semantics.~} A Labeled Transition System (LTS)\\
Let $\mathcal{A} = \mathcal{L} \cup \tau$ be the set of \str{actions}.  Below, $\alpha \in \mathcal{A}$.

$$
\inferrule[]{}{\sum_{i\in I} \pi_i.P_i \arro{~\pi_j~}  P_j ~~(j \in I)}   
\qquad
\inferrule[]{}{!\pi.P \arro{~\pi~}  P \parallel !\pi.P }
$$
$$
\inferrule[]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	
\quad
\inferrule[]{P \arro{~\alpha~} P' \andalso \alpha,\overline{\alpha} \text{ not in } \til{n}}{(\nu \til{n})P  \arro{~\alpha~}  (\nu \til{n})P'}
$$
$$
\fbox{
\inferrule[]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}
}
$$
}

\frame{
\frametitle{Our base language: Milner's CCS}
\str{Example:~}A process which emits a  signal $\outC{e}$ infinitely  often:
\begin{eqnarray*}
%\hspace{-7mm}
S & = & \outC{s} \parallel !s.\outC{a} \parallel !a.\outC{e}.\outC{s}  \pause \qquad \text{[synchronize on $s$, release $\outC{a}$]} \\ 
& \arro{~\tau~} &   \outC{a} \parallel !s.\outC{a} \parallel !a.\outC{e}.\outC{s} \pause \qquad \text{[synchronize on $a$, release $\outC{e}.\outC{s}$]}  \\
& \arro{~\tau~} &  !s.\outC{a} \parallel \outC{e}.\outC{s} \parallel !a.\outC{e}.\outC{s} \pause \qquad \text{[emit output  on $e$]} \\
 & \arro{~\outC{e}~} & \outC{s} \parallel !s.\outC{a} \parallel !a.\outC{e}.\outC{s}  \\
& = & S 
\end{eqnarray*}
}

\frame{
\frametitle{The process calculi approach, \underline{in our case}}
\begin{center}
%A \str{} to the analysis of \str{evolvable systems} 

%\pause

\bi
\item Identify some \str{phenomenon of interest} 
\item Isolate \str{basic construct(s)} for it, and define a \str{calculus}
\item Study the \str{properties} of the calculus (and systems modeled in it) and define \str{reasoning techniques} for it
\ei
\end{center}

\pause

Here, we are concerned with \emphcolor{dynamic reconfiguration} issues:\\
\begin{itemize}
\item finding proper \emphcolor{constructs} for representing evolution 
\item defining \emphcolor{correctness properties} for evolvable systems
\end{itemize}


%\pause
%
%\begin{block}{Our choices}
%\bi
%\item The phenomena: \str{components} and their \str{evolution}
%\item The calculus: $\mathcal{E}$, a core language with \str{updatable} components
%\item The properties: \str{(un)decidability} of component  \str{adaptation}
%\ei
%\end{block}

}

\frame{
\frametitle{Dynamic reconfiguration is important}
It is everywhere:
\bi
\item Software update (in OS, for instance)
\item Runtime reconfiguration in component-based systems
\item Workflow applications
\item Cloud computing
\item Structured communication
\item \dots
\ei

\pause 
\fkspc
\emphcolorb{Claim:} Existing process calculi do not properly capture dynamic reconfiguration.
}

%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%
%Essentially, the \emphcolor{underlying topology}: \pause 
%
%\begin{itemize}
%  \item CCS: interacting concurrent processes in a \str{static} topology
%  
%  \item The $\pi$-calculus: \str{dynamic communication} topologies through \emphcolor{channel/link mobility}
%%  \vspace{0.5cm}
%  
%  \item The Ambient calculus: \str{dynamic spatial} topologies through \emphcolor{ambient  mobility}
%  %(dynamic behaviours depending on the position)
%%\vspace{0.5cm}
%\end{itemize}
%
%
%%What about \emphcolor{dynamic reconfiguration}?
%%Dynamic reconfiguration does not really fit in any of these abstractions
%%  \item but what about dynamic behaviors? How to describe a process that changes along time?
%
%\end{frame}
%
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\ \pause
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility1.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility2.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility3.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility4.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility5.pdf}
%\end{center}
%\end{frame}
%
%\begin{frame}
%\frametitle{What is dynamic in known process calculi?}
%Reconfiguration is only possible at a \emphcolor{low, local} level. \\
%In $\pi$-calculus, only the linkage structure can be reconfigured:
%\begin{center}
%\includegraphics[height=40mm]{linkmobility6.pdf}
%\end{center} \pause
%What about \emphcolor{global} reconfiguration, performed \emphcolor{atomically}? \\
%(Say, relocating/replicating/hiding $P \parallel Q \parallel R$, \emphcolor{at once})
%\end{frame}




\section{Adaptable Processes}

\begin{frame}
\frametitle{Adaptable processes}
A process calculi approach to evolvable systems
\pause
\begin{itemize}
  \item Provide \emphcolor{direct control} on process execution 
  \item Processes can be stopped, restarted, relocated, at runtime 
  \item A form of \emphcolor{higher-order} process communication
\end{itemize}

\pause
\begin{block}{Our proposal}
\begin{enumerate}
\item A \emphcolor{process calculus} of adaptable processes, called \emphcolorb{\evol{}} \pause
\item \emphcolor{Verification problems} for evolvable systems defined in \evol{} \pause
\item \emphcolor{(Un)decidability results} for such problems
\end{enumerate}
\end{block}
\pause
In \str{this talk} I will  focus mainly on (1) and (2) 
\end{frame}

\begin{frame}
\frametitle{A calculus for adaptable processes }

\begin{block}{Syntax}
\visible<1,2,3,4>CCS without restriction \invisible<1>{plus \emphcolor{located processes}\\}\invisible<1,2>{ and \emphcolorb{update prefixes}:}
$$
\begin{array}{ll}
P        ::=& \sum_{i \in I} \pi_i.P_i   \, \midd \, 
          P \parallel P  \, \midd \, ! \pi.P \, \invisible<1>{\midd \, \emphcolor{\component{a}{P}}}\\ \\
\pi   ::=&  a \, \midd \, \outC{a} \invisible<1,2>{\, \midd \, \emphcolorb{\update{a}{U}}}
\end{array}
$$
\invisible<1,2,3>{where 
\begin{itemize}
\item $\component{a}{P}$ is the \emphcolor{adaptable process} $P$ \emphcolor{located at} name $a$
\item $U$ is a \emphcolorb{context}, with zero or more \emphcolorb{holes}, denoted $\bullet$
\end{itemize}}
\end{block}

\end{frame}








\begin{frame}
\frametitle{A calculus for adaptable processes}

\begin{block}{Operational Semantics: Intutions}
\begin{itemize}
\item Localities are \emphcolor{transparent}:
$$
 \rightinfer
 			{\component{a}{P} \xrightarrow{~\alpha~}  \component{a}{P'}}
 			{P \xrightarrow{~\alpha~} P'} 
			$$
			
\item Reconfiguration via \emphcolor{interaction}  with update prefixes:
$$
\component{a}{P} \parallel \update{a}{U}.Q \xrightarrow{~\tau~} \fillcon{U}{P} \parallel Q
$$
\pause 
\hspace{-6mm}
\small{[$\fillcon{U}{P}$ is the \emphcolor{process} obtained by filling in the holes in $U$ with $P$]}
%\item An update replaces an adaptable process with a
%new process filled with the process currently
%active in the updated location
%
%\end{itemize}
%
%metti sintassi di techrep
% $$
%\begin{array}{c}
% \component{a}{P} \xrightarrow{~\component{a}{P}~}  \star
%\qquad 
%\rightinfer
%			{P_1 \parallel P_2 \xrightarrow{~\tau~} P_1'\sub{ U \sub{Q}{\bullet}  }{\star} \parallel P_2'}
%			{P_1 \xrightarrow{~\component{a}{Q}~} P_1' \qquad P_2 \xrightarrow{~\update{a}{U}~} P_2'}
%\end{array}
%$$
\end{itemize}
\end{block}

\end{frame}

\frame{
\frametitle{A calculus for adaptable processes}
%\vspace{-4mm}
\begin{block}{Operational Semantics: LTS}
%\vspace{-6mm}
%A Labeled Transition System (LTS) which extends that of C
{\footnotesize
$$
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
%\fbox{\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}}
%\qquad 
%  \mathrm{\textsc{Upd}}~~~\update{a}{P_1}.P_2 \arro{\update{a}{P_1}}  P_2
%$$
%$$
\hidecolor{\inferrule[]{}{\sum_{i\in I} \alpha_i.P_i \arro{~\alpha_i~}  P_i } }
%\rightinfer	[\textsc{Rec}]
 %			{rec \,X.P \arro{\alpha} P}
 %			{P\sub{rec \, X.P}{X} \arro{\alpha} P'}
 %\quad
\qquad
\hidecolor{\inferrule[]{}{!\alpha.P \arro{~\alpha~}  P \parallel !\alpha.P }}
$$
$$
%\fbox{\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}}
%\quad 
\hidecolor{\inferrule[]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	}
\quad
\hidecolor{\inferrule[]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}}
$$
}
\pause
$$
\hspace{-8mm}
\fbox{
\inferrule[]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}
\quad  
\inferrule[]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}
\quad~~
\inferrule[]{P_1 \arro{~\component{a}{\emphcolor{Q}}~} P_1'\andalso P_2 \arro{~\update{a}{\emphcolorb{U}}~} P_2' }{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{\emphcolorb{U}}{\emphcolor{Q}}  }{\star} \parallel P_2'}~}
$$
\\ 
\hidecolor{[Reduction $\pired$ is defined as $\arro{~\tau~}$]}
\end{block}
}

\frame{
\frametitle{A first example}

A basic client-server scenario:  
\begin{eqnarray*}
C & = & \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.Q} \\
S & = & \componentbbig{server}{upd.\update{run}{\component{run}{R \parallel old.\bullet}}.S} 
\end{eqnarray*}

\pause

We then have two interactions, first on \emphcolor{$upd$} then on \emphcolor{$run$}:
\begin{align*}
%P & \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.C} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
C \parallel S \pired ~ & \componentbbig{client}{\component{run}{\emphcolor{P}} \parallel  Q} \parallel \componentbbig{server}{\update{run}{\str{\component{run}{R \parallel old.\bullet}}}.S} \\ 
\pired ~ & \componentbbig{client}{\str{\component{run}{R \parallel old.\emphcolor{P}}} \parallel Q} \parallel \componentbbig{server}{S}
\end{align*}

}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1-3>[Replacement] $$\quad \component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{R}}}.S \pired \str{\component{a}{R}} \parallel S  ~~(\bullet \not \in R)$$ 
\item<2-3>[Destroyer]$$\quad \component{a}{\emphcolor{Q}} \parallel \update{a}{\str{R}}.S \pired \str{R} \parallel S  ~~(\bullet \not \in R)$$ 
\item<3>[Plug-in] $$\component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{c{.}\bullet +R}}}.\nil \pired \str{\component{a}{c{.}\emphcolor{Q} +\fillcon{R}{\emphcolor{Q}}}} \parallel \nil$$ 
\end{description}
}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1-3>[Renaming] $$\componentbbig{m}{\component{a}{\emphcolor{Q}}} \parallel \componentbbig{n}{\update{a}{\str{\component{b}{\bullet}}}.S} \pired \componentbbig{m}{\str{\component{b}{\emphcolor{Q}}}}\parallel \componentbbig{n}{S}$$
\item<2-3>[Backup] $$\component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{\bullet}} \parallel \str{\component{b}{\bullet}}}.S \pired \str{\component{a}{\emphcolor{Q}}} \parallel \str{\component{b}{\emphcolor{Q}}} \parallel S$$
\item<3>[Deep update] $$\hspace{-55pt}\componentbbig{a}{Q \parallel \component{b}{R \parallel \emphcolor{\component{c}{S_{1}}}\, }\, } \parallel \update{c}{\str{\component{d}{S_{2}}}}.\nil \pired \componentbbig{a}{Q \parallel \componentbbig{b}{R \parallel \str{\component{d}{S_{2}}}\, }\, } \parallel \nil $$
\end{description}
}

\section{A Compelling Example}
\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}
 
% \begin{block}{}
%A workflow  describes how  a 
%number of activities coordinate to achieve a particular task.

A \str{workflow-based application}  consisting of 
\begin{enumerate}
\item  a \emphcolor{workflow engine (we)}  with workflows $\nm{W}_{1},  \ldots,  \nm{W}_{k}$ running on top of it. Each $\nm{W}_{i}$ contains several \emphcolor{activities}.
\item a \emphcolor{workflow base library (wbl)} to  support  running activities.
\item  \emphcolor{runtime services} $\nmu{S}_{1}, \ldots,  \nmu{S}_{m}$ implementing things like, e.g., transaction handling and external communication. 
\end{enumerate}

\pause

\fkspc

In \evol{}, this scenario may be represented as:
 $$
  App \midef \componentbig{\nm{wfa}}{\, \componentbbig{\nm{we}}{\nmu{WE} \parallel \underbrace{\nm{W}_{1} \parallel \cdots \parallel \nm{W}_{k}}_{\text{$k$ workflows}} \parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \prod_{l \in M}\nmu{S}_{l} \,}
 $$

\end{frame}

\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}

\str{Representing a single workflow}
\begin{itemize}
\item Each workflow $\nm{W}_{i}$ is an adaptable process $\nm{w}_{i}$
containing 
a process $\nmu{WL}_{i}$ (the \emphcolor{workflow's logic}) 
and 
$n$ \emphcolor{activities} 

\item Each activity is formalized as an adaptable process $\nm{a}_{j}$ 
and an \emphcolor{execution environment} $\nm{env}_{j}$:
%\todo{$ea_1$ stands for execution environment for $a_i$}
$$
\nm{W}_{i} = \componentbig{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n \underbrace{\big(\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}\big) }_{\text{$j$-th activity}}\,}
%\nm{W}_{i} = \component{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n (\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \component{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}) \,}
$$
\end{itemize}

\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}
%\vspace{-5mm}

%\emphcolor{Updating a single activity.~}
Let's specify the 
%We define 
%update actions on $\nm{a}_{j}$ to 
\emphcolor{update a single activity} within a workflow.
%model an update to the \emphcolor{reconfiguration mechanisms} for a single activity:
$$
\nm{W}_{i} = \componentbig{\nm{w}_{i}}{\,  \emphcolorm{\nmu{WL}_{i}} \parallel \prod_{j=1}^n \underbrace{\big(\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}\big) }_{\text{$j$-th activity}}\,}
%\nm{W}_{i} = \component{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n (\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \component{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}) \,}
$$
  \pause \\

%\fkspc

%An upgrade to the \emphcolor{reconfiguration mechanisms} of $\nm{W}_{i}$.
Suppose a process
$R_{1} = !\,\nm{replace}_{j}.\updatebig{\nm{a}_{j}}{\component{a_{j}}{!u_{j}.\update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \str{\nmu{newA}_{j}}}}}}$ \underline{inside 
$\emphcolorm{\nmu{WL}_{i}}$}. 

\fkspc

Given an output  at $\nm{replace}_{j}$, we obtain: 
$$
\nm{W}_{i} \pired \componentbig{\nm{w}_{i}}{\,  \emphcolorm{\nmu{WL}_{i}} \parallel \prod_{j=1}^n \big(\component{\nm{env}_j}{\nmu{P}_{j}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \str{\nmu{newA}_{j}}}}}\big) \,}
$$
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}
\frametitle{A compelling  example: workflow reconfiguration}
Let's specify the 
\emphcolor{suspension of a whole workflow} running in the workflow engine.
%Given our basic model, we can model \emphcolor{workflow suspension}  inside the workflow engine.
$$
App \midef \componentbig{\nm{wfa}}{\, \componentbbig{\nm{we}}{\emphcolorm{\nmu{WE}} \parallel \underbrace{\component{\nm{w}_{1}}{\nmu{WF}_{1}} \parallel \cdots \parallel \emphcolorm{\component{\nm{w}_{k}}{\nmu{WF}_{k}}}}_{\text{$k$ workflows}}\parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \prod_{l \in M} \nmu{S}_{l}}
 $$
 \pause
 
Suppose a  process \\
$
R_{2} = !\,\nm{suspend}_{k}.\updatebig{\nm{w}_{k}}{\str{\nm{go}_{k}.\component{\nm{w}_{k}}{\bullet}}}
$
 inside  \emphcolorm{\nmu{WE}}.

\pause 

\fkspc

Given an output at $\nm{suspend}_{i}$, 
$\component{\nm{w}_{k}}{\nmu{WF}_{k}}$ 
and $R_{2}$
may interact:
%$$\nm{resume}_{i}.\component{\nm{w}_{i}}{\nmu{WF}_{i}}$$
$$
\hspace{-7mm}
App \pired \componentbig{\nm{wfa}}{\, \componentbbig{\nm{we}}{\emphcolorm{\nmu{WE}} \parallel \underbrace{\component{\nm{w}_{1}}{\nmu{WF}_{1}} \parallel \cdots \parallel  \str{\nm{go}_{k}.\component{\nm{w}_{k}}{\emphcolorm{\nmu{WF}_{k}}}} }_{\text{$k$ workflows}}\parallel \component{\nm{\nm{wbl}}}{\nmu{BL}}} \parallel \prod_{l \in M} \nmu{S}_{l}}
 $$
%which can be reactivated at a later time.
\end{frame}



\section{Verification Problems}

\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables} 
\includegraphics[height=50mm]{cluster0.pdf}
\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster2.pdf}
\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster1.pdf}
\end{frame}

\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster3.pdf}
\end{frame}

\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}
%Distinguish between \emphcolor{correct} and \emphcolor{error} states, using \emphcolor{observables}
\includegraphics[height=50mm]{cluster4.pdf}
\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario: Intuitions}

%\emphcolor{Reachability of absence of errors}
Towards \emphcolor{general} correctness criteria for adaptable processes

\begin{itemize}
\item Systems as \str{clusters}:  an initial configuration plus reconfiguration actions
\item Define \str{undesirable observables} of the cluster's behavior
\item Correctness properties ensure such observables will \str{disappear}, possibly because of reconfigurations
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Verfication problems for adaptable processes}

An evolvable system is composed of an \emphcolor{initial configuration} and an arbitrary number of \emphcolorb{reconfiguration actions}\pause:
\begin{definition}[Cluster] 
Let $P, M_1,\ldots,M_n$ be processes s.t. $\mathcal{M}=\{M_1,\ldots,M_n\}$. \\
The set of \emphcolor{clusters} $\BC_P^\mathcal{M}$ is defined as:
$$\BC_P^\mathcal{M} = \big\{\emphcolor{P} \parallel \prod^{k_1} \emphcolorb{M_1} \parallel \dots \parallel \prod^{k_n} \emphcolorb{M_n} \mid k_1, \dots, k_n \in \mathbb{N} \big\}$$
\end{definition}

\end{frame}

\begin{frame}
\frametitle{Verfication problems for adaptable processes}

We observe the system's behavior using \emphcolor{barbs}. 

%\fkspc

%These observables may represent \emphcolor{errors}, but not necessarily so. 
%\pause

\begin{definition}[Barbs]\label{d:barb}
Let $P$ be a process, and let $\alpha$ be an action. 
\begin{itemize}
\item We write \emphcolor{$P \downarrow_{\alpha}$} if  $\exists P'. P \arro{~\alpha~} P'$ \pause

\item Given  $k > 0$, we write \emphcolor{$P\barb{\alpha}^{k}$}
iff \\
$\exists Q_{1},\ldots, Q_{k}$ s.t. 
$P \pired^{*} Q_1 \pired \ldots \pired Q_k$
with $Q_i \downarrow_\alpha$, $\forall i \in \{1,\ldots, k\}$. \qquad~~{\small\olivecolor{[That is, $k$ consecutive observables.]}} \pause 

\item We write \emphcolor{$P\barb{\alpha}^{\omega}$} iff  \\
%there exists an \emphcolor{infinite computation}
$\exists Q_{1}, Q_{2}, \ldots$ s.t. $P \pired^* Q_1 \pired Q_2 \pired  \ldots$
with $Q_i \downarrow_\alpha$, $\forall i \in \mathbb{N}$. 
\qquad\qquad~{\small \olivecolor{[That is, infinite consecutive observables.]} }\pause 
\end{itemize}

\fkspc

\begin{center}
\fbox{~~We  use \emphcolor{$\negbarbk{\alpha}$} and \emphcolor{$\negbarbw{\alpha}$} to denote the \emphcolor{negation} of $\barbk{\alpha}$ and $\barbw{\alpha}$.~~}
\end{center}
\end{definition}
\end{frame}




%\begin{frame}
%\frametitle{Verfication problems for adaptable processes}
%\str{Reachability of error absence} 
%\fkspc
%Given a set of clusters $\BC_P^\mathcal{M}$
%and a 
%barb \emphcolor{$e$}, 
%we would like to know if all computations of processes in $\BC_P^\mathcal{M}$
%\begin{itemize}
%\item have \emphcolor{at most $k$ consecutive states} exhibiting \emphcolor{$e$}, or
%\item  \emphcolor{eventually} reach a state in which \emphcolor{$e$} is not observable.
%\end{itemize}
%
%\end{frame}




\begin{frame}
\frametitle{Verfication problems for adaptable processes}

\begin{definition}[Adaptation Problems]
%Suppose an initial process $P$, a set of processes $M$, a barb $e$.

\begin{itemize}
\item  Given $k>0$, the \emphcolor{bounded adaptation} problem (\OG) consists in checking  
whether $\forall R \in \BC_P^\mathcal{M}$, \emphcolor{$R \, \negbarbk{e}$} holds.

\item The \emphcolor{eventual adaptation} problem (\LG) consists in checking  
whether   
$\forall R \in \BC_P^\mathcal{M}$,  \emphcolor{$R \, \negbarbw{e}$} holds.
\end{itemize}
\end{definition}
\end{frame}


\begin{frame}
\frametitle{The adaptation problems in the workflow example}

 Our model of a workflow:
 {\small 
$$
\hidecolor{\nm{W}_{i} = \componentbig{\nm{w}_{i}}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n \underbrace{\big(\component{\nm{env}_j}{\emphcolorm{\nmu{P}_{j}}} \parallel \componentbbig{\nm{a}_{j}}{ !u_j. \update{\nm{env}_j}{\component{\nm{env}_j}{\bullet \parallel \nmu{A}_{j}}}}\big) }_{\text{$j$-th activity}}\,}}
$$
}

Suppose $\emphcolorm{\nmu{P}_{j}}$ emits a signal representing an \str{urgent request}.\\
The signal is \emphcolor{repeatedly} emitted until the request is fulfilled. \\
Adaptation at $\nm{env}_j$ is expected as a response to the request.


% Suppose an emergency activity that executes inside the workflow
%process $\nmu{P}_{j}$ would emit a signal representing an urgent request, and 
%an update action  at $\nm{env}_j$ would represent a response to the emergency,
%implemented as process $\nmu{A}_{j}$.
%
\fkspc
Both \LG/\OG specify a future correct state of the workflow:
\begin{itemize}
\item While \LG says the request will be \emphcolor{eventually} fulfilled...
\item \OG says it  will be fulfilled \emphcolor{within a certain time bound}.
\end{itemize}
\end{frame}

\section{(Un)decidability Results for Adaptable Processes}

\begin{frame}
 \frametitle{Undecidability of the verification problems}

\OG and \LG  are \emphcolor{undecidable} in \evol{} \pause
\begin{itemize}

 \item The proof proceeds by relating both problems to \emphcolor{termination} in Turing complete models

 \item Let $M$ be a Turing machine, and $\encp{M}{}$ be its \evol{} encoding \\
If $M$ terminates then $\encp{M}{}$  has
a computation where an error  is \emphcolor{always available} \pause
 \end{itemize}
\vspace{3mm}
We model \str{two-counter machines}:
\begin{itemize}
 \item A counter is a \emphcolor{chain of input prefixes} located inside an adaptable process $c$. \quad 
 Example: $\component{c}{u.u.u.z}$ is number 3
 \item The increment \emphcolor{updates} $c$ enlarging the chain with an  $u$ 
\item The decrement is an \emphcolor{output} on $u$ that consumes one unit 
\end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Two-counter machine in \evol{}} 

Two-counter machines (aka Minsky machines) are a Turing complete model \\
\vspace{2mm}
\begin{tabular}{l}   
\(  
\mathrm{\textsc{Counter}}~c_j \qquad
\encp{c_j = n}{\mmn{}}   =  \component{c_j}{\encn{n}{j}} 
\)  \\%where
\quad where 
\quad  \(  
\encn{n}{j}=\left\{  
\begin{array}{ll}  
\overline{z_j}  & \textrm{if } n= 0 \\  
 \overline{u_j}.\encn{n-1}{j} & \textrm{if } n> 0 .  
\end{array}\right.  
\)
\\
\\ 
\(
\begin{array}{ll}   
\multicolumn{2}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(c_j))}{\mmn{}} \!&= !p_i.\update{c_j}{\component{c_j}{\overline{u_j}.\bullet}}.\overline{p_{i+1}}\\
\encp{(i: \mathtt{DECJ}(c_j,s))}{\mmn{}}\!&=  !p_i.(u_j.\overline{p_{i+1}} + z_j.\update{c_j}{\component{c_j}{\overline{z_j}}}.\overline{p_{s}})\\
\encp{(i: \mathtt{HALT})}{\mmn{}}\!&=  !p_i.(e + %.\update{c_0}{\component{c_0}{\overline{z_0}}}.\update{c_1}{\component{c_1}{\overline{z_1}}}
\outC{p_i})
\end{array}   
\)
\end{tabular}

\end{frame}


\frame{
\frametitle{(Un)decidability results for \evol{} processes }

But,  are there any  \emphcolor{fragments} of \evol{} where
 \OG /\LG are \emphcolor{decidable}? %\pause 
 \vspace{3mm}
 
%\begin{itemize}
%\item Decidability and expressiveness are interwoven questions

Perhaps we could restrict update actions
and obtain decidability?

\fkspc

\pause 

We consider two characterizations of \evol{} processes: 
\begin{description}
\item[Structural] Static and dynamic \emphcolor{topologies} of \evol{} proceses 
\item[Behavioral] Different \emphcolor{update patterns} (the $U$ in $\update{a}{U}$) 
\end{description}
%\item Six different variants of \evol{}
%\end{itemize} 
}

\frame{
\frametitle{(Un)decidability results for \evol{} processes }
\begin{block}{Structural Characterization}
The \emphcolor{topology} of evolvable systems is represented by the nesting of adaptable processes  (a tree-like structure)

\fkspc

\pause 
\str{\evols{}: Static \evol{}}
\bi 
\item The topology is \emphcolor{invariant} along reduction: \\
adaptable processes cannot be created/destroyed.
\item Enforced via syntactic/semantic restrictions
\item {\small (Replacement)}  $\quad \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(\bullet \not \in R)$
\ei 


\pause 
%\begin{description}
\str{\evold{}: Dynamic \evol{}} 
\bi 
\item All kinds of updates are allowed
\item {\small (Destroyer)} $\quad \componentbbig{c}{\component{a}{P} \parallel \update{a}{Q}.R} \pired \componentbbig{c}{Q \parallel R} \quad (\bullet \not \in Q)$
\ei



\fkspc

A process in \evols{} is in \evold{}, but the converse do not always hold.
\end{block}
}

\frame{
\frametitle{(Un)decidability results for \evol{} processes }
\begin{block}{Behavioral Characterization}
Restricting the $U$ in $\update{a}{U}$:
\begin{itemize}
\visible<1,4>{\item \evol{1}: all update patterns are allowed}
\visible<2,4>{\item \evol{2}: only update patterns with no $\bullet$  \emphcolor{behind prefixes}}
\visible<3,4>{\item \evol{3}: only update patterns in which $\bullet$  must \emphcolor{always occur} }
\end{itemize} 
\end{block}

%\pause 

%\begin{block}
\emphcolor{Non examples:}
\bi
\visible<2,4>{\item $\hidecolor{\text{(Plug-in)}}~~\component{a}{Q} \parallel \update{a}{\component{a}{c{.}\bullet +R}}.\nil \pired \component{a}{c{.}Q +\fillcon{R}{Q}} \parallel \nil$}
%\visible<2,4>{\item $\hidecolor{\text{(Destroyer)}}~~\quad \component{a}{P} \parallel \update{a}{Q}.R \pired Q \parallel R \quad (\bullet \not \in Q)$}
\visible<3,4>{\item$\hidecolor{\text{(Replacement)}}~\quad \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(\bullet \not \in R)$ }
\ei
%\end{block}
}


\frame{
\frametitle{Summary of (un)decidability results}

{\small
\begin{table}
%\begin{center}
%\hspace{-8mm}
\begin{tabular}{c|c|c}
		& \evold{} -- Dynamic Topology & \evols{} -- Static Topology \\
\hline \hline
\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
\hline
\evol{2}	& ~ \OG \emphcolor{decidable}~/~\LG undec ~ & ~ \OG \emphcolor{decidable}~/~\LG undec \\
\hline
\evol{3}	& ~ \OG \emphcolor{decidable}~/~\LG \str{undec} ~ & \OG~\emphcolor{decidable}~/~\LG \emphcolor{decidable} 
\end{tabular}
%\end{center}
\end{table}
}

\pause 

\begin{itemize}
\item Undecidability via encodings of \emphcolorb{two-counter machines} \pause

\item Decidability of $\OG$ via \emphcolorb{well-structured transition systems} \pause 

\item Decidability of $\LG$ via  a reduction to a \emphcolorb{place boundedness}, a decidable problem in Petri nets

\end{itemize} 

}



\section{Final Remarks}
\begin{frame}
\frametitle{Concluding remarks}

\begin{itemize}
\item 
A process calculus approach to dynamic reconfiguration and adaptation of concurrent systems
\item 
Two basic adaptation properties aimed at formalizing correctness with several scenarios 
\item 
A basis for the development of more expressive languages, and for verification studies
\end{itemize}

\fkspc

%\pause

%See the technical report at 
%\begin{center}
%\url{http://www.cs.unibo.it/~perez/ap/}
%\end{center}
%\begin{itemize}
%\item Extended examples
%\item Adaptable processes with \emphcolor{static} and \emphcolor{dynamic} topologies
%\end{itemize}

\end{frame}

\frame{
\frametitle{Ongoing and future work}

\begin{block}{Ongoing}
\bi
%\item 
%Decidability results for static and dynamic topologies of adaptable processes---forthcoming TR.

\item 
(Non-)encodability of \evol{} in the $\pi$-calculus  and in the higher-order $\pi$-calculus
%\item \OG and \LG in \str{opaque} adaptable processes with 
%\bi
%\item \emphcolor{capabilities} (e.g., ``$a$ cannot be updated from outside'') 
%\item  \emphcolor{multiplicities} (e.g., ``$a$ can be updated at most once'') 
%\ei
\ei
\end{block} 

\pause 

\begin{block}{Future}
\bi



%\item ``Structure preserving'' updates
%\item Update actions with \emphcolor{fairness} considerations


\item Adaptable processes and  disciplines for structured communication


\item Extensions: name/process passing, restriction, interfaces.


\item Complexity results for decidable properties

\ei
\end{block} 
}

\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}

\end{document}